Iof proof for Lemma add mono wrt le rw:
a, b, n:
. {(a 
b) 
((a+n) (b+n))}
by ((Unfold `guard` 0)
CollapseTHEN (Lemma `add_mono_wrt_le`))
C.| 12,41 |
a, b, n:. {(a b) ((a+n) (b+n))}
by ((Unfold `guard` 0)
CollapseTHEN (Lemma `add_mono_wrt_le`))
C.
| Definitions | |
| Lemmas |